es:ES, i:Id, xs:(Id List). state@i r state@i|xs 

latex

Definitions

ES, t  T, f(a), EState(T), Id, , x:AB(x), x:A. B(x), pred!(e;e'), SWellFounded(R(x;y)), Unit, Void, x:A.B(x), Top, S  T, left + right, Type, suptype(S; T), first(e), b, A, loc(e), <a, b>, s = t, P  Q, constant_function(f;A;B), IdLnk, x,y. t(x;y), x. t(x), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, x:A  B(x), P & Q, , r  s, e < e', val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), , Msg(M), type List, kind(e), EOrderAxioms(E; pred?; info), EqDecider(T), Atom$n, False, let x,y = A in B(x;y), vartype(i;x), IdDeq, , (x  l), b, a < b, P  Q, x:A. B(x), if b then t else f fi , x.A(x), deq-member(eq;x;L), state@i|xs, state@i

Lemmas

deq-member wf, id-deq wf, es-vartype wf, subtype rel dep function, ifthenelse wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-deq-member, bnot wf, l member wf, deq wf, EOrderAxioms wf, Id wf, kind wf, loc wf, Msg wf, nat wf, val-axiom wf, cless wf, qle wf, bool wf, rationals wf, Knd wf, kindcase wf, IdLnk wf, EState wf, constant function wf, not wf, assert wf, first wf, top wf, unit wf, event system wf